\begin{tabbing}
with decls ${\it ds}$ ${\it da}$sends on $l$ from $e$ include $f$($e$) and only these for tags in ${\it tgs}$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:es{-}E(${\it es}$). \+
\\[0ex]($\uparrow$es{-}isrcv(${\it es}$; $e$))
\\[0ex]$\Rightarrow$ (es{-}lnk(${\it es}$; $e$) = $l$)
\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:es{-}E(${\it es}$)\+
\\[0ex](($\uparrow$es{-}isrcv(${\it es}$; ${\it e'}$))
\\[0ex]c$\wedge$ \=((es{-}lnk(${\it es}$; ${\it e'}$) = $l$)\+
\\[0ex]$\wedge$ (es{-}tag(${\it es}$; ${\it e'}$) $\in$ ${\it tgs}$)
\\[0ex]$\wedge$ (es{-}sender(${\it es}$; ${\it e'}$) = es{-}sender(${\it es}$; $e$)))))
\-\-\\[0ex]$\Rightarrow$ (es{-}tag(${\it es}$; $e$) $\in$ ${\it tgs}$))
\\[0ex]c$\wedge$ \=(($\forall$${\it e'}$:es{-}E(${\it es}$). \+
\\[0ex]($\uparrow$es{-}isrcv(${\it es}$; ${\it e'}$))
\\[0ex]$\Rightarrow$ (es{-}lnk(${\it es}$; ${\it e'}$) = $l$)
\\[0ex]$\Rightarrow$ (es{-}tag(${\it es}$; ${\it e'}$) $\in$ ${\it tgs}$)
\\[0ex]$\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; ${\it e'}$); fpf{-}cap(${\it da}$; Kind{-}deq; es{-}kind(${\it es}$; ${\it e'}$); void)))
\\[0ex]$\wedge$ ($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; source($l$); $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top))))
\-\\[0ex]c$\wedge$ \=(alle{-}at(\=${\it es}$;\+\+
\\[0ex]source($l$);
\\[0ex]$e$.($\forall$$i$:int\_seg(0; $\parallel$$f$($e$)$\parallel$). 
\\[0ex]$\exists$\=${\it e'}$:es{-}E(${\it es}$)\+
\\[0ex](($\uparrow$es{-}isrcv(${\it es}$; ${\it e'}$))
\\[0ex]$\wedge$ (es{-}lnk(${\it es}$; ${\it e'}$) = $l$)
\\[0ex]$\wedge$ (es{-}tag(${\it es}$; ${\it e'}$) $\in$ ${\it tgs}$)
\\[0ex]$\wedge$ (es{-}sender(${\it es}$; ${\it e'}$) = $e$)
\\[0ex]$\wedge$ (es{-}index(${\it es}$; ${\it e'}$) = $i$))))
\-\-\\[0ex]$\wedge$ \=($\forall$${\it e'}$:es{-}E(${\it es}$). \+
\\[0ex]($\uparrow$es{-}isrcv(${\it es}$; ${\it e'}$))
\\[0ex]$\Rightarrow$ (es{-}lnk(${\it es}$; ${\it e'}$) = $l$)
\\[0ex]$\Rightarrow$ (es{-}tag(${\it es}$; ${\it e'}$) $\in$ ${\it tgs}$)
\\[0ex]$\Rightarrow$ \=((es{-}index(${\it es}$; ${\it e'}$) $<$ $\parallel$$f$(es{-}sender(${\it es}$; ${\it e'}$))$\parallel$)\+
\\[0ex]c$\wedge$ (\=$<$es{-}tag(${\it es}$; ${\it e'}$), es{-}val(${\it es}$; ${\it e'}$)$>$\+
\\[0ex]=
\\[0ex]$f$(es{-}sender(${\it es}$; ${\it e'}$))[es{-}index(${\it es}$; ${\it e'}$)]))))
\-\-\-\-\-
\end{tabbing}